package net.greyar.theory;

import java.util.List;
import java.util.Map;

public class Variable extends Symbol {
	public Variable(String token) {
		this.token = "?" + Variable.id();
		this.print = token;
	}
	@Override
	protected StringBuilder toString(StringBuilder sb) {
		sb.append(token);
		return sb;
	}
	@Override
	protected StringBuilder getPrint(StringBuilder sb) {
		sb.append(print);
		return sb;
	}
	@Override
	public boolean occurs(Variable variable) {
		return this == variable;
	}
	@Override
	public Substitution unify(Symbol other, Substitution sigma) {
		if (other instanceof Literal || other instanceof Variable || other instanceof Expression) {
			if (sigma.bound(this)) {
				return sigma.get(this).unify(other, sigma);
			}
			if (sigma.bound(other)) {
				return unify(sigma.get(other), sigma);
			}
			if (sigma.constrained(this)) {
				return sigma.satisfy(this, other);
			}
			if (sigma.constrained(other)) {
				return sigma.satisfy(other, this);
			}
			if (this != other && !other.occurs(this)) {
				return sigma.bind(this, other);
			}
			return sigma;
		}
		return other.unify(this, sigma);
	}
	@Override
	public Symbol apply(Substitution sigma, Map<String, Variable> variables) {
		Symbol last = sigma.last(this);
		if (last instanceof Variable) {
			if (!variables.containsKey(last.getPrint())) {
				variables.put(last.getPrint(), new Variable(last.getPrint()));
			}
			return variables.get(last.getPrint());
		}
		return last.apply(sigma, variables);
	}
	@Override
	protected List<Variable> getVariables(List<Variable> variables) {
		variables.add(this);
		return variables;
	}
	private static long id = 0;
	private static String id() {
		if (id == Long.MAX_VALUE) {
			id = Long.MIN_VALUE;
		}
		return String.valueOf(++id);
	}
	@Override
	protected Symbol level() {
		return this;
	}
	@Override
	protected boolean grounds(Substitution sigma) {
		Symbol last = sigma.last(this);
		if (last instanceof Variable) {
			return false;
		}
		return last.grounds(sigma);
	}
	@Override
	public String getKey() {
		return token;
	}
}
